<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>5. Elementary Number Theory &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="6. Discrete Mathematics" href="C06_Discrete_Mathematics.html" />
    <link rel="prev" title="4. Sets and Functions" href="C04_Sets_and_Functions.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">5. Elementary Number Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#irrational-roots">5.1. Irrational Roots</a></li>
<li class="toctree-l2"><a class="reference internal" href="#induction-and-recursion">5.2. Induction and Recursion</a></li>
<li class="toctree-l2"><a class="reference internal" href="#infinitely-many-primes">5.3. Infinitely Many Primes</a></li>
<li class="toctree-l2"><a class="reference internal" href="#more-induction">5.4. More Induction</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">5. </span>Elementary Number Theory</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C05_Elementary_Number_Theory.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="elementary-number-theory">
<span id="number-theory"></span><h1><span class="section-number">5. </span>Elementary Number Theory<a class="headerlink" href="#elementary-number-theory" title="Link to this heading">&#61633;</a></h1>
<p>In this chapter, we show you how to formalize some elementary
results in number theory.
As we deal with more substantive mathematical content,
the proofs will get longer and more involved,
building on the skills you have already mastered.</p>
<section id="irrational-roots">
<span id="section-irrational-roots"></span><h2><span class="section-number">5.1. </span>Irrational Roots<a class="headerlink" href="#irrational-roots" title="Link to this heading">&#61633;</a></h2>
<p>Let&#8217;s start with a fact known to the ancient Greeks, namely,
that the square root of 2 is irrational.
If we suppose otherwise,
we can write <span class="math notranslate nohighlight">\(\sqrt{2} = a / b\)</span> as a fraction
in lowest terms. Squaring both sides yields <span class="math notranslate nohighlight">\(a^2 = 2 b^2\)</span>,
which implies that <span class="math notranslate nohighlight">\(a\)</span> is even.
If we write <span class="math notranslate nohighlight">\(a = 2c\)</span>, then we get <span class="math notranslate nohighlight">\(4c^2 = 2 b^2\)</span>
and hence <span class="math notranslate nohighlight">\(b^2 = 2 c^2\)</span>.
This implies that <span class="math notranslate nohighlight">\(b\)</span> is also even, contradicting
the fact that we have assumed that <span class="math notranslate nohighlight">\(a / b\)</span> has been
reduced to lowest terms.</p>
<p>Saying that <span class="math notranslate nohighlight">\(a / b\)</span> is a fraction in lowest terms means
that <span class="math notranslate nohighlight">\(a\)</span> and <span class="math notranslate nohighlight">\(b\)</span> do not have any factors in common,
which is to say, they are <em>coprime</em>.
Mathlib defines the predicate <code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span> <span class="pre">m</span> <span class="pre">n</span></code> to be <code class="docutils literal notranslate"><span class="pre">Nat.gcd</span> <span class="pre">m</span> <span class="pre">n</span> <span class="pre">=</span> <span class="pre">1</span></code>.
Using Lean&#8217;s anonymous projection notation, if <code class="docutils literal notranslate"><span class="pre">s</span></code> and <code class="docutils literal notranslate"><span class="pre">t</span></code> are
expressions of type <code class="docutils literal notranslate"><span class="pre">Nat</span></code>, we can write <code class="docutils literal notranslate"><span class="pre">s.Coprime</span> <span class="pre">t</span></code> instead of
<code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span> <span class="pre">s</span> <span class="pre">t</span></code>, and similarly for <code class="docutils literal notranslate"><span class="pre">Nat.gcd</span></code>.
As usual, Lean will often unfold the definition of <code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span></code> automatically
when necessary,
but we can also do it manually by rewriting or simplifying with
the identifier <code class="docutils literal notranslate"><span class="pre">Nat.Coprime</span></code>.
The <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> tactic is smart enough to compute concrete values.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#print</span><span class="w"> </span><span class="n">Nat.Coprime</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.Coprime</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Coprime</span><span class="w"> </span><span class="mi">12</span><span class="w"> </span><span class="mi">7</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.gcd</span><span class="w"> </span><span class="mi">12</span><span class="w"> </span><span class="mi">8</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>
</pre></div>
</div>
<p>We have already encountered the <code class="docutils literal notranslate"><span class="pre">gcd</span></code> function in
<a class="reference internal" href="C02_Basics.html#more-on-order-and-divisibility"><span class="std std-numref">Section 2.4</span></a>.
There is also a version of <code class="docutils literal notranslate"><span class="pre">gcd</span></code> for the integers;
we will return to a discussion of the relationship between
different number systems below.
There are even a generic <code class="docutils literal notranslate"><span class="pre">gcd</span></code> function and generic
notions of <code class="docutils literal notranslate"><span class="pre">Prime</span></code> and <code class="docutils literal notranslate"><span class="pre">Coprime</span></code>
that make sense in general classes of algebraic structures.
We will come to understand how Lean manages this generality
in the next chapter.
In the meanwhile, in this section, we will restrict attention
to the natural numbers.</p>
<p>We also need the notion of a prime number, <code class="docutils literal notranslate"><span class="pre">Nat.Prime</span></code>.
The theorem <code class="docutils literal notranslate"><span class="pre">Nat.prime_def_lt</span></code> provides one familiar characterization,
and <code class="docutils literal notranslate"><span class="pre">Nat.Prime.eq_one_or_self_of_dvd</span></code> provides another.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Nat.prime_def_lt</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rwa</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.prime_def_lt</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">prime_p</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Nat.Prime.eq_one_or_self_of_dvd</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">prime_p.eq_one_or_self_of_dvd</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="mi">17</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>

<span class="c1">-- commonly used</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.prime_two</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.prime_three</span>
</pre></div>
</div>
<p>In the natural numbers, a prime number has the property that it cannot
be written as a product of nontrivial factors.
In a broader mathematical context, an element of a ring that has this property
is said to be <em>irreducible</em>.
An element of a ring is said to be <em>prime</em> if whenever it divides a product,
it divides one of the factors.
It is an important property of the natural numbers
that in that setting the two notions coincide,
giving rise to the theorem <code class="docutils literal notranslate"><span class="pre">Nat.Prime.dvd_mul</span></code>.</p>
<p>We can use this fact to establish a key property in the argument
above:
if the square of a number is even, then that number is even as well.
Mathlib defines the predicate <code class="docutils literal notranslate"><span class="pre">Even</span></code> in <code class="docutils literal notranslate"><span class="pre">Algebra.Group.Even</span></code>,
but for reasons that will become clear below,
we will simply use <code class="docutils literal notranslate"><span class="pre">2</span> <span class="pre">&#8739;</span> <span class="pre">m</span></code> to express that <code class="docutils literal notranslate"><span class="pre">m</span></code> is even.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Nat.Prime.dvd_mul</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.Prime.dvd_mul</span><span class="w"> </span><span class="n">Nat.prime_two</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.prime_two.dvd_mul</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">even_of_even_sqr</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">pow_two</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.prime_two.dvd_mul</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">cases</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">assumption</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.Prime.dvd_of_dvd_pow</span><span class="w"> </span><span class="n">Nat.prime_two</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>As we proceed, you will need to become proficient at finding the facts you
need.
Remember that if you can guess the prefix of the name and
you have imported the relevant library,
you can use tab completion (sometimes with <code class="docutils literal notranslate"><span class="pre">ctrl-tab</span></code>) to find
what you are looking for.
You can use <code class="docutils literal notranslate"><span class="pre">ctrl-click</span></code> on any identifier to jump to the file
where it is defined, which enables you to browse definitions and theorems
nearby.
You can also use the search engine on the
<a class="reference external" href="https://leanprover-community.github.io/">Lean community web pages</a>,
and if all else fails,
don&#8217;t hesitate to ask on
<a class="reference external" href="https://leanprover.zulipchat.com/">Zulip</a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="c1">-- apply? suggests the following:</span>
<span class="w">  </span><span class="o">(</span><span class="n">mul_right_inj&#39;</span><span class="w"> </span><span class="n">h&#39;</span><span class="o">)</span><span class="bp">.</span><span class="n">mp</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The heart of our proof of the irrationality of the square root of two
is contained in the following theorem.
See if you can fill out the proof sketch, using
<code class="docutils literal notranslate"><span class="pre">even_of_even_sqr</span></code> and the theorem <code class="docutils literal notranslate"><span class="pre">Nat.dvd_gcd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">coprime_mn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">sqr_eq</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">meq</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">dvd_iff_exists_eq_mul_left.mp</span><span class="w"> </span><span class="n">this</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">sqr_eq</span><span class="o">,</span><span class="w"> </span><span class="n">meq</span><span class="o">]</span>
<span class="w">    </span><span class="n">ring</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">m.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">norm_num</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
</pre></div>
</div>
<p>In fact, with very few changes, we can replace <code class="docutils literal notranslate"><span class="pre">2</span></code> by an arbitrary prime.
Give it a try in the next example.
At the end of the proof, you&#8217;ll need to derive a contradiction from
<code class="docutils literal notranslate"><span class="pre">p</span> <span class="pre">&#8739;</span> <span class="pre">1</span></code>.
You can use <code class="docutils literal notranslate"><span class="pre">Nat.Prime.two_le</span></code>, which says that
any prime number is greater than or equal to two,
and <code class="docutils literal notranslate"><span class="pre">Nat.le_of_dvd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">coprime_mn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Coprime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Let us consider another approach.
Here is a quick proof that if <span class="math notranslate nohighlight">\(p\)</span> is prime, then
<span class="math notranslate nohighlight">\(m^2 \ne p n^2\)</span>: if we assume <span class="math notranslate nohighlight">\(m^2 = p n^2\)</span>
and consider the factorization of <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span> into primes,
then <span class="math notranslate nohighlight">\(p\)</span> occurs an even number of times on the left side of the equation
and an odd number of times on the right, a contradiction.
Note that this argument requires that <span class="math notranslate nohighlight">\(n\)</span> and hence <span class="math notranslate nohighlight">\(m\)</span>
are not equal to zero.
The formalization below confirms that this assumption is sufficient.</p>
<p>The unique factorization theorem says that any natural number other
than zero can be written as the product of primes in a unique way.
Mathlib contains a formal version of this, expressed in terms of a function
<code class="docutils literal notranslate"><span class="pre">Nat.primeFactorsList</span></code>, which returns the list of
prime factors of a number in nondecreasing order.
The library proves that all the elements of <code class="docutils literal notranslate"><span class="pre">Nat.primeFactorsList</span> <span class="pre">n</span></code>
are prime, that any <code class="docutils literal notranslate"><span class="pre">n</span></code> greater than zero is equal to the
product of its factors,
and that if <code class="docutils literal notranslate"><span class="pre">n</span></code> is equal to the product of another list of prime numbers,
then that list is a permutation of <code class="docutils literal notranslate"><span class="pre">Nat.primeFactorsList</span> <span class="pre">n</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Nat.primeFactorsList</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.prime_of_mem_primeFactorsList</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.prod_primeFactorsList</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.primeFactorsList_unique</span>
</pre></div>
</div>
<p>You can browse these theorems and others nearby, even though we have not
talked about list membership, products, or permutations yet.
We won&#8217;t need any of that for the task at hand.
We will instead use the fact that Mathlib has a function <code class="docutils literal notranslate"><span class="pre">Nat.factorization</span></code>,
that represents the same data as a function.
Specifically, <code class="docutils literal notranslate"><span class="pre">Nat.factorization</span> <span class="pre">n</span> <span class="pre">p</span></code>, which we can also write
<code class="docutils literal notranslate"><span class="pre">n.factorization</span> <span class="pre">p</span></code>, returns the multiplicity of <code class="docutils literal notranslate"><span class="pre">p</span></code> in the prime
factorization of <code class="docutils literal notranslate"><span class="pre">n</span></code>. We will use the following three facts.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">factorization_mul&#39;</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">mnez</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">nnez</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.factorization_mul</span><span class="w"> </span><span class="n">mnez</span><span class="w"> </span><span class="n">nnez</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">factorization_pow&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.factorization_pow</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">Nat.Prime.factorization&#39;</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">p.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">prime_p.factorization</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>In fact, <code class="docutils literal notranslate"><span class="pre">n.factorization</span></code> is defined in Lean as a function of finite support,
which explains the strange notation you will see as you step through the
proofs above. Don&#8217;t worry about this now. For our purposes here, we can use
the three theorems above as a black box.</p>
<p>The next example shows that the simplifier is smart enough to replace
<code class="docutils literal notranslate"><span class="pre">n^2</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code> by <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code>. The tactic <code class="docutils literal notranslate"><span class="pre">simpa</span></code> just calls <code class="docutils literal notranslate"><span class="pre">simp</span></code>
followed by <code class="docutils literal notranslate"><span class="pre">assumption</span></code>.</p>
<p>See if you can use the identities above to fill in the missing parts
of the proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">nnz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">sqr_eq</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">nsqr_nez</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.factorization</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">eq1</span><span class="o">,</span><span class="w"> </span><span class="n">sqr_eq</span><span class="o">,</span><span class="w"> </span><span class="n">eq2</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.add_mul_mod_self_left</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.mul_mod_right</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
<span class="w">  </span><span class="n">norm_num</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
</pre></div>
</div>
<p>A nice thing about this proof is that it also generalizes. There is
nothing special about <code class="docutils literal notranslate"><span class="pre">2</span></code>; with small changes, the proof shows that
whenever we write <code class="docutils literal notranslate"><span class="pre">m^k</span> <span class="pre">=</span> <span class="pre">r</span> <span class="pre">*</span> <span class="pre">n^k</span></code>, the multiplicity of any prime <code class="docutils literal notranslate"><span class="pre">p</span></code>
in <code class="docutils literal notranslate"><span class="pre">r</span></code> has to be a multiple of <code class="docutils literal notranslate"><span class="pre">k</span></code>.</p>
<p>To use <code class="docutils literal notranslate"><span class="pre">Nat.count_factors_mul_of_pos</span></code> with <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">*</span> <span class="pre">n^k</span></code>,
we need to know that <code class="docutils literal notranslate"><span class="pre">r</span></code> is positive.
But when <code class="docutils literal notranslate"><span class="pre">r</span></code> is zero, the theorem below is trivial, and easily
proved by the simplifier.
So the proof is carried out in cases.
The line <code class="docutils literal notranslate"><span class="pre">rcases</span> <span class="pre">r</span> <span class="pre">with</span> <span class="pre">_</span> <span class="pre">|</span> <span class="pre">r</span></code> replaces the goal with two versions:
one in which <code class="docutils literal notranslate"><span class="pre">r</span></code> is replaced by <code class="docutils literal notranslate"><span class="pre">0</span></code>,
and the other in which <code class="docutils literal notranslate"><span class="pre">r</span></code> is replaces by <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">+</span> <span class="pre">1</span></code>.
In the second case, we can use the theorem <code class="docutils literal notranslate"><span class="pre">r.succ_ne_zero</span></code>, which
establishes <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">+</span> <span class="pre">1</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code> (<code class="docutils literal notranslate"><span class="pre">succ</span></code> stands for successor).</p>
<p>Notice also that the line that begins <code class="docutils literal notranslate"><span class="pre">have</span> <span class="pre">:</span> <span class="pre">npow_nz</span></code> provides a
short proof-term proof of <code class="docutils literal notranslate"><span class="pre">n^k</span> <span class="pre">&#8800;</span> <span class="pre">0</span></code>.
To understand how it works, try replacing it with a tactic proof,
and then think about how the tactics describe the proof term.</p>
<p>See if you can fill in the missing parts of the proof below.
At the very end, you can use <code class="docutils literal notranslate"><span class="pre">Nat.dvd_sub'</span></code> and <code class="docutils literal notranslate"><span class="pre">Nat.dvd_mul_right</span></code>
to finish it off.</p>
<p>Note that this example does not assume that <code class="docutils literal notranslate"><span class="pre">p</span></code> is prime, but the
conclusion is trivial when <code class="docutils literal notranslate"><span class="pre">p</span></code> is not prime since <code class="docutils literal notranslate"><span class="pre">r.factorization</span> <span class="pre">p</span></code>
is then zero by definition, and the proof works in all cases anyway.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">nnz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">pow_eq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">r.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">r</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">npow_nz</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">npowz</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">nnz</span><span class="w"> </span><span class="o">(</span><span class="n">pow_eq_zero</span><span class="w"> </span><span class="n">npowz</span><span class="o">)</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">eq2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">((</span><span class="n">r</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span>
<span class="w">      </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="bp">.</span><span class="n">factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r.succ.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n.factorization</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">eq1</span><span class="o">,</span><span class="w"> </span><span class="n">pow_eq</span><span class="o">,</span><span class="w"> </span><span class="n">eq2</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.add_sub_cancel</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">this</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>There are a number of ways in which we might want to improve on these results.
To start with, a proof that the square root of two is irrational
should say something about the square root of two,
which can be understood as an element of the
real or complex numbers.
And stating that it is irrational should say something about the
rational numbers, namely, that no rational number is equal to it.
Moreover, we should extend the theorems in this section to the integers.
Although it is mathematically obvious that if we could write the square root of
two as a quotient of two integers then we could write it as a quotient
of two natural numbers,
proving this formally requires some effort.</p>
<p>In Mathlib, the natural numbers, the integers, the rationals, the reals,
and the complex numbers are represented by separate data types.
Restricting attention to the separate domains is often helpful:
we will see that it is easy to do induction on the natural numbers,
and it is easiest to reason about divisibility of integers when the
real numbers are not part of the picture.
But having to mediate between the different domains is a headache,
one we will have to contend with.
We will return to this issue later in this chapter.</p>
<p>We should also expect to be able to strengthen the conclusion of the
last theorem to say that the number <code class="docutils literal notranslate"><span class="pre">r</span></code> is a <code class="docutils literal notranslate"><span class="pre">k</span></code>-th power,
since its <code class="docutils literal notranslate"><span class="pre">k</span></code>-th root is just the product of each prime dividing <code class="docutils literal notranslate"><span class="pre">r</span></code>
raised to its multiplicity in <code class="docutils literal notranslate"><span class="pre">r</span></code> divided by <code class="docutils literal notranslate"><span class="pre">k</span></code>.
To be able to do that we will need better means for reasoning about
products and sums over a finite set,
which is also a topic we will return to.</p>
<p>In fact, the results in this section are all established in much
greater generality in Mathlib,
in <code class="docutils literal notranslate"><span class="pre">Data.Real.Irrational</span></code>.
The notion of <code class="docutils literal notranslate"><span class="pre">multiplicity</span></code> is defined for an
arbitrary commutative monoid,
and that it takes values in the extended natural numbers <code class="docutils literal notranslate"><span class="pre">enat</span></code>,
which adds the value infinity to the natural numbers.
In the next chapter, we will begin to develop the means to
appreciate the way that Lean supports this sort of generality.</p>
</section>
<section id="induction-and-recursion">
<span id="section-induction-and-recursion"></span><h2><span class="section-number">5.2. </span>Induction and Recursion<a class="headerlink" href="#induction-and-recursion" title="Link to this heading">&#61633;</a></h2>
<p>The set of natural numbers <span class="math notranslate nohighlight">\(\mathbb{N} = \{ 0, 1, 2, \ldots \}\)</span>
is not only fundamentally important in its own right,
but also a plays a central role in the construction of new mathematical objects.
Lean&#8217;s foundation allows us to declare <em>inductive types</em>,
which are types generated inductively by a given list of
<em>constructors</em>.
In Lean, the natural numbers are declared as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span><span class="w"> </span><span class="n">Nat</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span>
</pre></div>
</div>
<p>You can find this in the library by writing <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">Nat</span></code> and
then using <code class="docutils literal notranslate"><span class="pre">ctrl-click</span></code> on the identifier <code class="docutils literal notranslate"><span class="pre">Nat</span></code>.
The command specifies that <code class="docutils literal notranslate"><span class="pre">Nat</span></code> is the datatype generated
freely and inductively by the two constructors <code class="docutils literal notranslate"><span class="pre">zero</span> <span class="pre">:</span> <span class="pre">Nat</span></code> and
<code class="docutils literal notranslate"><span class="pre">succ</span> <span class="pre">:</span> <span class="pre">Nat</span> <span class="pre">&#8594;</span> <span class="pre">Nat</span></code>.
Of course, the library introduces notation <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> and <code class="docutils literal notranslate"><span class="pre">0</span></code> for
<code class="docutils literal notranslate"><span class="pre">nat</span></code> and <code class="docutils literal notranslate"><span class="pre">zero</span></code> respectively. (Numerals are translated to binary
representations, but we don&#8217;t have to worry about the details of that now.)</p>
<p>What &#8220;freely&#8221; means for the working mathematician is that the type
<code class="docutils literal notranslate"><span class="pre">Nat</span></code> has an element <code class="docutils literal notranslate"><span class="pre">zero</span></code> and an injective successor function
<code class="docutils literal notranslate"><span class="pre">succ</span></code> whose image does not include <code class="docutils literal notranslate"><span class="pre">zero</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n.succ</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">Nat.zero</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.succ_ne_zero</span><span class="w"> </span><span class="n">n</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.succ</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n.succ</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Nat.succ.inj</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>What the word &#8220;inductively&#8221; means for the working mathematician is that
the natural numbers comes with a principle of proof by induction
and a principle of definition by recursion.
This section will show you how to use these.</p>
<p>Here is an example of a recursive definition of the factorial
function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span>
</pre></div>
</div>
<p>The syntax takes some getting used to.
Notice that there is no <code class="docutils literal notranslate"><span class="pre">:=</span></code> on the first line.
The next two lines provide the base case and inductive step
for a recursive definition.
These equations hold definitionally, but they can also
be used manually by giving the name <code class="docutils literal notranslate"><span class="pre">fac</span></code> to <code class="docutils literal notranslate"><span class="pre">simp</span></code> or <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
</pre></div>
</div>
<p>The factorial function is actually already defined in Mathlib as
<code class="docutils literal notranslate"><span class="pre">Nat.factorial</span></code>. Once again, you can jump to it by typing
<code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">Nat.factorial</span></code> and using <code class="docutils literal notranslate"><span class="pre">ctrl-click.</span></code>
For illustrative purposes, we will continue using <code class="docutils literal notranslate"><span class="pre">fac</span></code> in the examples.
The annotation <code class="docutils literal notranslate"><span class="pre">&#64;[simp]</span></code> before the definition
of <code class="docutils literal notranslate"><span class="pre">Nat.factorial</span></code> specifies that
the defining equation should be added to the database of identities
that the simplifier uses by default.</p>
<p>The principle of induction says that we can prove a general statement
about the natural numbers by proving that the statement holds of 0
and that whenever it holds of a natural number <span class="math notranslate nohighlight">\(n\)</span>,
it also holds of <span class="math notranslate nohighlight">\(n + 1\)</span>.
The line <code class="docutils literal notranslate"><span class="pre">induction'</span> <span class="pre">n</span> <span class="pre">with</span> <span class="pre">n</span> <span class="pre">ih</span></code> in the proof
below therefore results in two goals:
in the first we need to prove <code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">fac</span> <span class="pre">0</span></code>,
and in the second we have the added assumption <code class="docutils literal notranslate"><span class="pre">ih</span> <span class="pre">:</span> <span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">fac</span> <span class="pre">n</span></code>
and a required to prove <code class="docutils literal notranslate"><span class="pre">0</span> <span class="pre">&lt;</span> <span class="pre">fac</span> <span class="pre">(n</span> <span class="pre">+</span> <span class="pre">1)</span></code>.
The phrase <code class="docutils literal notranslate"><span class="pre">with</span> <span class="pre">n</span> <span class="pre">ih</span></code> serves to name the variable and
the assumption for the inductive hypothesis,
and you can choose whatever names you want for them.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fac_pos</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">zero_lt_one</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">mul_pos</span><span class="w"> </span><span class="n">n.succ_pos</span><span class="w"> </span><span class="n">ih</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">induction'</span></code> tactic is smart enough to include hypotheses
that depend on the induction variable as part of the
induction hypothesis.
Step through the next example to see what is going on.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">dvd_fac</span><span class="w"> </span><span class="o">{</span><span class="n">i</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">ipos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">ile</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">exact</span><span class="w"> </span><span class="n">absurd</span><span class="w"> </span><span class="n">ipos</span><span class="w"> </span><span class="o">(</span><span class="n">not_lt_of_ge</span><span class="w"> </span><span class="n">ile</span><span class="o">)</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">Nat.of_le_succ</span><span class="w"> </span><span class="n">ile</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_of_dvd_right</span><span class="w"> </span><span class="o">(</span><span class="n">ih</span><span class="w"> </span><span class="n">h</span><span class="o">)</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">h</span><span class="o">]</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_right</span>
</pre></div>
</div>
<p>The following example provides a crude lower bound for the factorial
function.
It turns out to be easier to start with a proof by cases,
so that the remainder of the proof starts with the case
<span class="math notranslate nohighlight">\(n = 1\)</span>.
See if you can complete the argument with a proof by induction using <code class="docutils literal notranslate"><span class="pre">pow_succ</span></code>
or <code class="docutils literal notranslate"><span class="pre">pow_succ'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">pow_two_le_fac</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Induction is often used to prove identities involving finite sums and
products.
Mathlib defines the expressions <code class="docutils literal notranslate"><span class="pre">Finset.sum</span> <span class="pre">s</span> <span class="pre">f</span></code> where
<code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Finset</span> <span class="pre">&#945;</span></code> is a finite set of elements of the type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and
<code class="docutils literal notranslate"><span class="pre">f</span></code> is a function defined on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
The codomain of <code class="docutils literal notranslate"><span class="pre">f</span></code> can be any type that supports a commutative,
associative addition operation with a zero element.
If you import <code class="docutils literal notranslate"><span class="pre">Algebra.BigOperators.Ring</span></code> and issue the command
<code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">BigOperators</span></code>, you can use the more suggestive notation
<code class="docutils literal notranslate"><span class="pre">&#8721;</span> <span class="pre">x</span> <span class="pre">&#8712;</span> <span class="pre">s,</span> <span class="pre">f</span> <span class="pre">x</span></code>. Of course, there is an analogous operation and
notation for finite products.</p>
<p>We will talk about the <code class="docutils literal notranslate"><span class="pre">Finset</span></code> type and the operations
it supports in the next section, and again in a later chapter.
For now, we will only make use
of <code class="docutils literal notranslate"><span class="pre">Finset.range</span> <span class="pre">n</span></code>, which is the finite set of natural numbers
less than <code class="docutils literal notranslate"><span class="pre">n</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Finset.sum</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">f</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Finset.prod</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">f</span>

<span class="kn">open</span><span class="w"> </span><span class="n">BigOperators</span>
<span class="kn">open</span><span class="w"> </span><span class="n">Finset</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s.sum</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s.prod</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">sum</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">prod</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p>The facts <code class="docutils literal notranslate"><span class="pre">Finset.sum_range_zero</span></code> and <code class="docutils literal notranslate"><span class="pre">Finset.sum_range_succ</span></code>
provide a recursive description of summation up to <span class="math notranslate nohighlight">\(n\)</span>,
and similarly for products.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.sum_range_zero</span><span class="w"> </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n.succ</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.sum_range_succ</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.prod_range_zero</span><span class="w"> </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n.succ</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.prod_range_succ</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">n</span>
</pre></div>
</div>
<p>The first identity in each pair holds definitionally, which is to say,
you can replace the proofs by <code class="docutils literal notranslate"><span class="pre">rfl</span></code>.</p>
<p>The following expresses the factorial function that we defined as a product.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">,</span><span class="w"> </span><span class="n">prod_range_zero</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">,</span><span class="w"> </span><span class="n">prod_range_succ</span><span class="o">,</span><span class="w"> </span><span class="n">mul_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>The fact that we include <code class="docutils literal notranslate"><span class="pre">mul_comm</span></code> as a simplification rule deserves
comment.
It should seem dangerous to simplify with the identity <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">y</span> <span class="pre">*</span> <span class="pre">x</span></code>,
which would ordinarily loop indefinitely.
Lean&#8217;s simplifier is smart enough to recognize that, and applies the rule
only in the case where the resulting term has a smaller value in some
fixed but arbitrary ordering of the terms.
The following example shows that simplifying using the three rules
<code class="docutils literal notranslate"><span class="pre">mul_assoc</span></code>, <code class="docutils literal notranslate"><span class="pre">mul_comm</span></code>, and <code class="docutils literal notranslate"><span class="pre">mul_left_comm</span></code>
manages to identify products that are the same up to the
placement of parentheses and ordering of variables.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">))</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">mul_comm</span><span class="o">,</span><span class="w"> </span><span class="n">mul_left_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>Roughly, the rules work by pushing parentheses to the right
and then re-ordering the expressions on both sides until they
both follow the same canonical order. Simplifying with these
rules, and the corresponding rules for addition, is a handy trick.</p>
<p>Returning to summation identities, we suggest stepping through the following proof
that the sum of the natural numbers up to and including <span class="math notranslate nohighlight">\(n\)</span> is
<span class="math notranslate nohighlight">\(n (n + 1) / 2\)</span>.
The first step of the proof clears the denominator.
This is generally useful when formalizing identities,
because calculations with division generally have side conditions.
(It is similarly useful to avoid using subtraction on the natural numbers when possible.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sum_id</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">),</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">symm</span><span class="bp">;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Nat.div_eq_of_eq_mul_right</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Finset.sum_range_succ</span><span class="o">,</span><span class="w"> </span><span class="n">mul_add</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>We encourage you to prove the analogous identity for sums of squares,
and other identities you can find on the web.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sum_sqr</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">),</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">6</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>In Lean&#8217;s core library, addition and multiplication are themselves defined
using recursive definitions,
and their fundamental properties are established using induction.
If you like thinking about foundational topics like that,
you might enjoy working through proofs
of the commutativity and associativity of multiplication and addition
and the distributivity of multiplication over addition.
You can do this on a copy of the natural numbers
following the outline below.
Notice that we can use the <code class="docutils literal notranslate"><span class="pre">induction</span></code> tactic with <code class="docutils literal notranslate"><span class="pre">MyNat</span></code>;
Lean is smart enough to know to
use the relevant induction principle (which is, of course,
the same as that for <code class="docutils literal notranslate"><span class="pre">Nat</span></code>).</p>
<p>We start you off with the commutativity of addition.
A good rule of thumb is that because addition and multiplication
are defined by recursion on the second argument,
it is generally advantageous to do proofs by induction on a variable
that occurs in that position.
It is a bit tricky to decide which variable to use in the proof
of associativity.</p>
<p>It can be confusing to write things without the usual notation
for zero, one, addition, and multiplication.
We will learn how to define such notation later.
Working in the namespace <code class="docutils literal notranslate"><span class="pre">MyNat</span></code> means that we can write
<code class="docutils literal notranslate"><span class="pre">zero</span></code> and <code class="docutils literal notranslate"><span class="pre">succ</span></code> rather than <code class="docutils literal notranslate"><span class="pre">MyNat.zero</span></code> and <code class="docutils literal notranslate"><span class="pre">MyNat.succ</span></code>,
and that these interpretations of the names take precedence over
others.
Outside the namespace, the full name of the <code class="docutils literal notranslate"><span class="pre">add</span></code> defined below,
for example, is <code class="docutils literal notranslate"><span class="pre">MyNat.add</span></code>.</p>
<p>If you find that you <em>really</em> enjoy this sort of thing, try defining
truncated subtraction and exponentiation and proving some of their
properties as well.
Remember that truncated subtraction cuts off at zero.
To define that, it is useful to define a predecessor function, <code class="docutils literal notranslate"><span class="pre">pred</span></code>,
that subtracts one from any nonzero number and fixes zero.
The function <code class="docutils literal notranslate"><span class="pre">pred</span></code> can be defined by a simple instance of recursion.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">inductive</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span>

<span class="kn">namespace</span><span class="w"> </span><span class="n">MyNat</span>

<span class="kd">def</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>

<span class="kd">def</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">MyNat</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">zero</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="n">x</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_add</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">succ_add</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">succ</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">zero_add</span><span class="o">]</span>
<span class="w">    </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add</span><span class="o">,</span><span class="w"> </span><span class="n">succ_add</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_add</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">(</span><span class="n">add</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">k</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">zero_mul</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">succ_mul</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="o">(</span><span class="n">succ</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="o">(</span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_comm</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MyNat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mul</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span><span class="w"> </span><span class="n">MyNat</span>
</pre></div>
</div>
</section>
<section id="infinitely-many-primes">
<span id="section-infinitely-many-primes"></span><h2><span class="section-number">5.3. </span>Infinitely Many Primes<a class="headerlink" href="#infinitely-many-primes" title="Link to this heading">&#61633;</a></h2>
<p>Let us continue our exploration of induction and recursion with another
mathematical standard: a proof that there are infinitely many primes.
One way to formulate this is as the statement that
for every natural number
<span class="math notranslate nohighlight">\(n\)</span>, there is a prime number greater than <span class="math notranslate nohighlight">\(n\)</span>.
To prove this, let <span class="math notranslate nohighlight">\(p\)</span> be any prime factor of <span class="math notranslate nohighlight">\(n! + 1\)</span>.
If <span class="math notranslate nohighlight">\(p\)</span> is less than or equal to <span class="math notranslate nohighlight">\(n\)</span>, it divides <span class="math notranslate nohighlight">\(n!\)</span>.
Since it also divides <span class="math notranslate nohighlight">\(n! + 1\)</span>, it divides 1, a contradiction.
Hence <span class="math notranslate nohighlight">\(p\)</span> is greater than <span class="math notranslate nohighlight">\(n\)</span>.</p>
<p>To formalize that proof, we need to show that any number greater than or equal
to 2 has a prime factor.
To do that, we will need to show that any natural number that is
not equal to 0 or 1 is greater-than or equal to 2.
And this brings us to a quirky feature of formalization:
it is often trivial statements like this that are among the most
annoying to formalize.
Here we consider a few ways to do it.</p>
<p>To start with, we can use the <code class="docutils literal notranslate"><span class="pre">cases</span></code> tactic and the fact that the
successor function respects the ordering on the natural numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">cases</span><span class="w"> </span><span class="n">m</span><span class="bp">;</span><span class="w"> </span><span class="n">contradiction</span>
<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">cases</span><span class="w"> </span><span class="n">m</span><span class="bp">;</span><span class="w"> </span><span class="n">contradiction</span>
<span class="w">    </span><span class="n">repeat</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">Nat.succ_le_succ</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">zero_le</span>
</pre></div>
</div>
<p>Another strategy is to use the tactic <code class="docutils literal notranslate"><span class="pre">interval_cases</span></code>,
which automatically splits the goal into cases when
the variable in question is contained in an interval
of natural numbers or integers.
Remember that you can hover over it to see its documentation.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">interval_cases</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">contradiction</span>
</pre></div>
</div>
<p id="index-0">Recall that the semicolon after <code class="docutils literal notranslate"><span class="pre">interval_cases</span> <span class="pre">m</span></code> means
that the next tactic is applied to each of the cases that it generates.
Yet another option is to use the tactic <code class="docutils literal notranslate"><span class="pre">decide</span></code>, which tries
to find a decision procedure to solve the problem.
Lean knows that you can decide the truth value of a statement that
begins with a bounded quantifier <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">x,</span> <span class="pre">x</span> <span class="pre">&lt;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">...</span></code> or <code class="docutils literal notranslate"><span class="pre">&#8707;</span> <span class="pre">x,</span> <span class="pre">x</span> <span class="pre">&lt;</span> <span class="pre">n</span> <span class="pre">&#8743;</span> <span class="pre">...</span></code>
by deciding each of the finitely many instances.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">revert</span><span class="w"> </span><span class="n">h0</span><span class="w"> </span><span class="n">h1</span>
<span class="w">  </span><span class="n">revert</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">m</span>
<span class="w">  </span><span class="n">decide</span>
</pre></div>
</div>
<p>With the theorem <code class="docutils literal notranslate"><span class="pre">two_le</span></code> in hand, let&#8217;s start by showing that every
natural number greater than two has a prime divisor.
Mathlib contains a function <code class="docutils literal notranslate"><span class="pre">Nat.minFac</span></code> that
returns the smallest prime divisor,
but for the sake of learning new parts of the library,
we&#8217;ll avoid using it and prove the theorem directly.</p>
<p>Here, ordinary induction isn&#8217;t enough.
We want to use <em>strong induction</em>, which allows us to prove
that every natural number <span class="math notranslate nohighlight">\(n\)</span> has a property <span class="math notranslate nohighlight">\(P\)</span>
by showing that for every number <span class="math notranslate nohighlight">\(n\)</span>, if <span class="math notranslate nohighlight">\(P\)</span> holds
of all values less than <span class="math notranslate nohighlight">\(n\)</span>, it holds at <span class="math notranslate nohighlight">\(n\)</span> as well.
In Lean, this principle is called <code class="docutils literal notranslate"><span class="pre">Nat.strong_induction_on</span></code>,
and we can use the <code class="docutils literal notranslate"><span class="pre">using</span></code> keyword to tell the induction tactic
to use it.
Notice that when we do that, there is no base case; it is subsumed
by the general induction step.</p>
<p>The argument is simply as follows. Assuming <span class="math notranslate nohighlight">\(n &#8805; 2\)</span>,
if <span class="math notranslate nohighlight">\(n\)</span> is prime, we&#8217;re done. If it isn&#8217;t,
then by one of the characterizations of what it means to be a prime number,
it has a nontrivial factor, <span class="math notranslate nohighlight">\(m\)</span>,
and we can apply the inductive hypothesis to that.
Step through the next proof to see how that plays out.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">exists_prime_factor</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n.Prime</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Nat.strong_induction_on</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.prime_def_lt</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mltn</span><span class="o">,</span><span class="w"> </span><span class="n">mdvdn</span><span class="o">,</span><span class="w"> </span><span class="n">mne1</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">mz</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mz</span><span class="o">,</span><span class="w"> </span><span class="n">zero_dvd_iff</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">mdvdn</span>
<span class="w">    </span><span class="n">linarith</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="n">mne1</span>
<span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Prime</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mp</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rcases</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">mltn</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">pdvd.trans</span><span class="w"> </span><span class="n">mdvdn</span>
</pre></div>
</div>
<p>We can now prove the following formulation of our theorem.
See if you can fill out the sketch.
You can use <code class="docutils literal notranslate"><span class="pre">Nat.factorial_pos</span></code>, <code class="docutils literal notranslate"><span class="pre">Nat.dvd_factorial</span></code>,
and <code class="docutils literal notranslate"><span class="pre">Nat.dvd_sub'</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">primes_infinite</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Nat.factorial</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">exists_prime_factor</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">refine</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="bp">?</span><span class="n">_</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">ple</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">ple</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">Nat.factorial</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">False</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Let&#8217;s consider a variation of the proof above, where instead
of using the factorial function,
we suppose that we are given by a finite set
<span class="math notranslate nohighlight">\(\{ p_1, \ldots, p_n \}\)</span> and we consider a prime factor of
<span class="math notranslate nohighlight">\(\prod_{i = 1}^n p_i + 1\)</span>.
That prime factor has to be distinct from each
<span class="math notranslate nohighlight">\(p_i\)</span>, showing that there is no finite set that contains
all the prime numbers.</p>
<p>Formalizing this argument requires us to reason about finite
sets. In Lean, for any type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, the type <code class="docutils literal notranslate"><span class="pre">Finset</span> <span class="pre">&#945;</span></code>
represents finite sets of elements of type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.
Reasoning about finite sets computationally requires having
a procedure to test equality on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, which is why the snippet
below includes the assumption <code class="docutils literal notranslate"><span class="pre">[DecidableEq</span> <span class="pre">&#945;]</span></code>.
For concrete data types like <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>, <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>, and <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>,
the assumption is satisfied automatically. When reasoning about
the real numbers, it can be satisfied using classical logic
and abandoning the computational interpretation.</p>
<p>We use the command <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">Finset</span></code> to avail ourselves of shorter names
for the relevant theorems. Unlike the case with sets,
most equivalences involving finsets do not hold definitionally,
so they need to be expanded manually using equivalences like
<code class="docutils literal notranslate"><span class="pre">Finset.subset_iff</span></code>, <code class="docutils literal notranslate"><span class="pre">Finset.mem_union</span></code>, <code class="docutils literal notranslate"><span class="pre">Finset.mem_inter</span></code>,
and <code class="docutils literal notranslate"><span class="pre">Finset.mem_sdiff</span></code>. The <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic can still be used
to show that two finite sets are equal by showing
that every element of one is an element of the other.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Finset</span>

<span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">subset_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mem_inter</span><span class="o">,</span><span class="w"> </span><span class="n">mem_union</span><span class="o">,</span><span class="w"> </span><span class="n">mem_union</span><span class="o">,</span><span class="w"> </span><span class="n">mem_inter</span><span class="o">,</span><span class="w"> </span><span class="n">mem_inter</span><span class="o">]</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">subset_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">subset_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="n">simp</span>
<span class="w">  </span><span class="n">tauto</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>We have used a new trick: the <code class="docutils literal notranslate"><span class="pre">tauto</span></code> tactic (and a strengthened
version, <code class="docutils literal notranslate"><span class="pre">tauto!</span></code>, which uses classical logic) can be used to
dispense with propositional tautologies. See if you can use
these methods to prove the two examples below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">\</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="bp">\</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">\</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="n">t</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>The theorem <code class="docutils literal notranslate"><span class="pre">Finset.dvd_prod_of_mem</span></code> tells us that if an
<code class="docutils literal notranslate"><span class="pre">n</span></code> is an element of a finite set <code class="docutils literal notranslate"><span class="pre">s</span></code>, then <code class="docutils literal notranslate"><span class="pre">n</span></code> divides
<code class="docutils literal notranslate"><span class="pre">&#8719;</span> <span class="pre">i</span> <span class="pre">&#8712;</span> <span class="pre">s,</span> <span class="pre">i</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Finset.dvd_prod_of_mem</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We also need to know that the converse holds in the case where
<code class="docutils literal notranslate"><span class="pre">n</span></code> is prime and <code class="docutils literal notranslate"><span class="pre">s</span></code> is a set of primes.
To show that, we need the following lemma, which you should
be able to prove using the theorem <code class="docutils literal notranslate"><span class="pre">Nat.Prime.eq_one_or_self_of_dvd</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">_root_.Nat.Prime.eq_of_dvd_of_prime</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span>
<span class="w">      </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">prime_q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We can use this lemma to show that if a prime <code class="docutils literal notranslate"><span class="pre">p</span></code> divides a product of a finite
set of primes, then it is equal to one of them.
Mathlib provides a useful principle of induction on finite sets:
to show that a property holds of an arbitrary finite set <code class="docutils literal notranslate"><span class="pre">s</span></code>,
show that it holds of the empty set, and show that it is preserved
when we add a single new element <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">&#8713;</span> <span class="pre">s</span></code>.
The principle is known as <code class="docutils literal notranslate"><span class="pre">Finset.induction_on</span></code>.
When we tell the induction tactic to use it, we can also specify the names
<code class="docutils literal notranslate"><span class="pre">a</span></code> and <code class="docutils literal notranslate"><span class="pre">s</span></code>, the name for the assumption <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">&#8713;</span> <span class="pre">s</span></code> in the inductive step,
and the name of the inductive hypothesis.
The expression <code class="docutils literal notranslate"><span class="pre">Finset.insert</span> <span class="pre">a</span> <span class="pre">s</span></code> denotes the union of <code class="docutils literal notranslate"><span class="pre">s</span></code> with the singleton <code class="docutils literal notranslate"><span class="pre">a</span></code>.
The identities <code class="docutils literal notranslate"><span class="pre">Finset.prod_empty</span></code> and <code class="docutils literal notranslate"><span class="pre">Finset.prod_insert</span></code> then provide
the relevant rewrite rules for the product.
In the proof below, the first <code class="docutils literal notranslate"><span class="pre">simp</span></code> applies <code class="docutils literal notranslate"><span class="pre">Finset.prod_empty</span></code>.
Step through the beginning of the proof to see the induction unfold,
and then finish it off.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">mem_of_dvd_prod_primes</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">prime_p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Finset.induction_on</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">ans</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">    </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">prime_p.two_le</span><span class="o">]</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Finset.prod_insert</span><span class="w"> </span><span class="n">ans</span><span class="o">,</span><span class="w"> </span><span class="n">prime_p.dvd_mul</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mem_insert</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We need one last property of finite sets.
Given an element <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">&#945;</span></code> and a predicate
<code class="docutils literal notranslate"><span class="pre">P</span></code> on <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, in  <a class="reference internal" href="C04_Sets_and_Functions.html#sets-and-functions"><span class="std std-numref">Chapter 4</span></a>
we wrote <code class="docutils literal notranslate"><span class="pre">{</span> <span class="pre">x</span> <span class="pre">&#8712;</span> <span class="pre">s</span> <span class="pre">|</span> <span class="pre">P</span> <span class="pre">x</span> <span class="pre">}</span></code> for the set of
elements of <code class="docutils literal notranslate"><span class="pre">s</span></code> that satisfy <code class="docutils literal notranslate"><span class="pre">P</span></code>.
Given <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Finset</span> <span class="pre">&#945;</span></code>,
the analogous notion is written <code class="docutils literal notranslate"><span class="pre">s.filter</span> <span class="pre">P</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s.filter</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">x.Prime</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mem_filter</span>
</pre></div>
</div>
<p>We now prove an alternative formulation of the statement that there are infinitely many
primes, namely, that given any <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">:</span> <span class="pre">Finset</span> <span class="pre">&#8469;</span></code>, there is a prime <code class="docutils literal notranslate"><span class="pre">p</span></code> that is not
an element of <code class="docutils literal notranslate"><span class="pre">s</span></code>.
Aiming for a contradiction, we assume that all the primes are in <code class="docutils literal notranslate"><span class="pre">s</span></code>, and then
cut down to a set <code class="docutils literal notranslate"><span class="pre">s'</span></code> that contains all and only the primes.
Taking the product of that set, adding one, and finding a prime factor
of the result
leads to the contradiction we are looking for.
See if you can complete the sketch below.
You can use <code class="docutils literal notranslate"><span class="pre">Finset.prod_pos</span></code> in the proof of the first <code class="docutils literal notranslate"><span class="pre">have</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">primes_infinite&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8713;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">s</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">s&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">s.filter</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">s&#39;_def</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mem_s&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">},</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s&#39;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">n.Prime</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">s&#39;_def</span><span class="o">]</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">exists_prime_factor</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">convert</span><span class="w"> </span><span class="n">Nat.dvd_sub</span><span class="w"> </span><span class="n">pdvd</span><span class="w"> </span><span class="n">this</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">False</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We have thus seen two ways of saying that there are infinitely many primes:
saying that they are not bounded by any <code class="docutils literal notranslate"><span class="pre">n</span></code>, and saying that they are
not contained in any finite set <code class="docutils literal notranslate"><span class="pre">s</span></code>.
The two proofs below show that these formulations are equivalent.
In the second, in order to form <code class="docutils literal notranslate"><span class="pre">s.filter</span> <span class="pre">Q</span></code>, we have to assume that there
is a procedure for deciding whether or not <code class="docutils literal notranslate"><span class="pre">Q</span></code> holds. Lean knows that there
is a procedure for <code class="docutils literal notranslate"><span class="pre">Nat.Prime</span></code>. In general, if we use classical logic
by writing <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">Classical</span></code>,
we can dispense with the assumption.</p>
<p>In Mathlib, <code class="docutils literal notranslate"><span class="pre">Finset.sup</span> <span class="pre">s</span> <span class="pre">f</span></code> denotes the supremum of the values of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> as <code class="docutils literal notranslate"><span class="pre">x</span></code>
ranges over <code class="docutils literal notranslate"><span class="pre">s</span></code>, returning <code class="docutils literal notranslate"><span class="pre">0</span></code> in the case where <code class="docutils literal notranslate"><span class="pre">s</span></code> is empty and
the codomain of <code class="docutils literal notranslate"><span class="pre">f</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>. In the first proof, we use <code class="docutils literal notranslate"><span class="pre">s.sup</span> <span class="pre">id</span></code>,
where <code class="docutils literal notranslate"><span class="pre">id</span></code> is the identity function, to refer to the maximum value in <code class="docutils literal notranslate"><span class="pre">s</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">bounded_of_ex_finset</span><span class="w"> </span><span class="o">(</span><span class="n">Q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="kt">Prop</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">hs</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="n">s.sup</span><span class="w"> </span><span class="n">id</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">Qk</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Nat.lt_succ_of_le</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="n">id</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">s.sup</span><span class="w"> </span><span class="n">id</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_sup</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="n">Qk</span><span class="o">)</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">ex_finset_of_bounded</span><span class="w"> </span><span class="o">(</span><span class="n">Q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="kt">Prop</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">DecidablePred</span><span class="w"> </span><span class="n">Q</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">Q</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">hn</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="o">(</span><span class="n">range</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">))</span><span class="bp">.</span><span class="n">filter</span><span class="w"> </span><span class="n">Q</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">k</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.lt_succ_iff</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">hn</span><span class="w"> </span><span class="n">k</span>
</pre></div>
</div>
<p>A small variation on our second proof that there are infinitely many primes
shows that there are infinitely many primes congruent to 3 modulo 4.
The argument goes as follows.
First, notice that if the product of two numbers <span class="math notranslate nohighlight">\(m\)</span> and <span class="math notranslate nohighlight">\(n\)</span>
is equal to 3 modulo 4, then one of the two numbers is congruent to 3 modulo 4.
After all, both have to be odd, and if they are both congruent to 1 modulo 4,
so is their product.
We can use this observation to show that if some number
greater than 2 is congruent to 3 modulo 4,
then that number has a prime divisor that is also congruent to 3 modulo 4.</p>
<p>Now suppose there are only finitely many prime numbers congruent to 3
modulo 4, say, <span class="math notranslate nohighlight">\(p_1, \ldots, p_k\)</span>.
Without loss of generality, we can assume that <span class="math notranslate nohighlight">\(p_1 = 3\)</span>.
Consider the product <span class="math notranslate nohighlight">\(4 \prod_{i = 2}^k p_i + 3\)</span>.
It is easy to see that this is congruent to 3 modulo 4, so it has
a prime factor <span class="math notranslate nohighlight">\(p\)</span> congruent to 3 modulo 4.
It can&#8217;t be the case that <span class="math notranslate nohighlight">\(p = 3\)</span>; since <span class="math notranslate nohighlight">\(p\)</span>
divides <span class="math notranslate nohighlight">\(4 \prod_{i = 2}^k p_i + 3\)</span>, if <span class="math notranslate nohighlight">\(p\)</span>
were equal to 3 then it would also divide <span class="math notranslate nohighlight">\(\prod_{i = 2}^k p_i\)</span>,
which implies that <span class="math notranslate nohighlight">\(p\)</span> is equal to
one of the <span class="math notranslate nohighlight">\(p_i\)</span> for <span class="math notranslate nohighlight">\(i = 2, \ldots, k\)</span>;
and we have excluded 3 from this list.
So <span class="math notranslate nohighlight">\(p\)</span> has to be one of the other elements <span class="math notranslate nohighlight">\(p_i\)</span>.
But in that case, <span class="math notranslate nohighlight">\(p\)</span> divides <span class="math notranslate nohighlight">\(4 \prod_{i = 2}^k p_i\)</span>
and hence 3, which contradicts the fact that it is not 3.</p>
<p>In Lean, the notation <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">%</span> <span class="pre">m</span></code>, read &#8220;<code class="docutils literal notranslate"><span class="pre">n</span></code> modulo <code class="docutils literal notranslate"><span class="pre">m</span></code>,&#8221;
denotes the remainder of the division of <code class="docutils literal notranslate"><span class="pre">n</span></code> by <code class="docutils literal notranslate"><span class="pre">m</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">27</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>
</pre></div>
</div>
<p>We can then render the statement &#8220;<code class="docutils literal notranslate"><span class="pre">n</span></code> is congruent to 3 modulo 4&#8221;
as <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">%</span> <span class="pre">4</span> <span class="pre">=</span> <span class="pre">3</span></code>. The following example and theorems sum up
the facts about this function that we will need to use below.
The first named theorem is another illustration of reasoning by
a small number of cases.
In the second named theorem, remember that the semicolon means that
the subsequent tactic block is applied to all the goals created by the
preceding tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.add_mul_mod_self_left</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mod_4_eq_3_or_mod_4_eq_3</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">revert</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.mul_mod</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Nat.mod_lt</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">interval_cases</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="bp">-</span><span class="n">Nat.mul_mod_mod</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Nat.mod_lt</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">(</span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span><span class="o">)</span>
<span class="w">  </span><span class="n">interval_cases</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">two_le_of_mod_4_eq_3</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="bp">&lt;;&gt;</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">intro</span><span class="w"> </span><span class="n">neq</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">neq</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">      </span><span class="n">norm_num</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We will also need the following fact, which says that if
<code class="docutils literal notranslate"><span class="pre">m</span></code> is a nontrivial divisor of <code class="docutils literal notranslate"><span class="pre">n</span></code>, then so is <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">/</span> <span class="pre">m</span></code>.
See if you can complete the proof using <code class="docutils literal notranslate"><span class="pre">Nat.div_dvd_of_dvd</span></code>
and <code class="docutils literal notranslate"><span class="pre">Nat.div_lt_self</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">aux</span><span class="w"> </span><span class="o">{</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Now put all the pieces together to prove that any
number congruent to 3 modulo 4 has a prime divisor with that
same property.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">exists_prime_factor_mod_4_eq_3</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n.Prime</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Nat.strong_induction_on</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.prime_def_lt</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">np</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">np</span><span class="w"> </span><span class="o">(</span><span class="n">two_le_of_mod_4_eq_3</span><span class="w"> </span><span class="n">h</span><span class="o">)</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mltn</span><span class="o">,</span><span class="w"> </span><span class="n">mdvdn</span><span class="o">,</span><span class="w"> </span><span class="n">mne1</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mge2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">mne1</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">mz</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mz</span><span class="o">,</span><span class="w"> </span><span class="n">zero_dvd_iff</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">mdvdn</span>
<span class="w">    </span><span class="n">linarith</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">neq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Nat.mul_div_cancel&#39;</span><span class="w"> </span><span class="n">mdvdn</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">mod_4_eq_3_or_mod_4_eq_3</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">neq</span><span class="o">,</span><span class="w"> </span><span class="n">h</span><span class="o">]</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">h1</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">h1</span>
<span class="w">  </span><span class="bp">.</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">.</span><span class="w"> </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We are in the home stretch. Given a set <code class="docutils literal notranslate"><span class="pre">s</span></code> of prime
numbers, we need to talk about the result of removing 3 from that
set, if it is present. The function <code class="docutils literal notranslate"><span class="pre">Finset.erase</span></code> handles that.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rwa</span><span class="w"> </span><span class="o">[</span><span class="n">mem_erase</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">assumption</span>
</pre></div>
</div>
<p>We are now ready to prove that there are infinitely many primes
congruent to 3 modulo 4.
Fill in the missing parts below.
Our solution uses <code class="docutils literal notranslate"><span class="pre">Nat.dvd_add_iff_left</span></code> and <code class="docutils literal notranslate"><span class="pre">Nat.dvd_sub'</span></code>
along the way.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">primes_mod_4_eq_3_infinite</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">by_contra</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">push_neg</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">hn</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">ex_finset_of_bounded</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">contrapose</span><span class="bp">!</span><span class="w"> </span><span class="n">hn</span>
<span class="w">    </span><span class="n">rcases</span><span class="w"> </span><span class="n">hn</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">p4</span><span class="o">&#10217;,</span><span class="w"> </span><span class="n">pltn</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pltn</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">p4</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">hs</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">((</span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">3</span><span class="o">)</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">exists_prime_factor_mod_4_eq_3</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">,</span><span class="w"> </span><span class="n">p4eq</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">ps</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">pne3</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">erase</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">contradiction</span>
</pre></div>
</div>
<p>If you managed to complete the proof, congratulations! This has been a serious
feat of formalization.</p>
</section>
<section id="more-induction">
<span id="id1"></span><h2><span class="section-number">5.4. </span>More Induction<a class="headerlink" href="#more-induction" title="Link to this heading">&#61633;</a></h2>
<p>In <a class="reference internal" href="#section-induction-and-recursion"><span class="std std-numref">Section 5.2</span></a>, we saw how to define the factorial function by
recursion on the natural numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span>
</pre></div>
</div>
<p>We also saw how to prove theorems using the <code class="docutils literal notranslate"><span class="pre">induction'</span></code> tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fac_pos</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction&#39;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">zero_lt_one</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">mul_pos</span><span class="w"> </span><span class="n">n.succ_pos</span><span class="w"> </span><span class="n">ih</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">induction</span></code> tactic (without the prime tick mark) allows for more structured syntax.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">zero_lt_one</span>
<span class="w">  </span><span class="n">case</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">mul_pos</span><span class="w"> </span><span class="n">n.succ_pos</span><span class="w"> </span><span class="n">ih</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">zero_lt_one</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">mul_pos</span><span class="w"> </span><span class="n">n.succ_pos</span><span class="w"> </span><span class="n">ih</span>
</pre></div>
</div>
<p>As usual, you can hover over the <code class="docutils literal notranslate"><span class="pre">induction</span></code> keyword to read the documentation.
The names of the cases, <code class="docutils literal notranslate"><span class="pre">zero</span></code> and <code class="docutils literal notranslate"><span class="pre">succ</span></code>, are taken from the definition of the type <cite>&#8469;</cite>.
Notice that the <code class="docutils literal notranslate"><span class="pre">succ</span></code> case allows you to choose whatever names you want for the
induction variable and the inductive hypothesis, here <code class="docutils literal notranslate"><span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">ih</span></code>.
You can even prove a theorem with the same notation used to define a recursive function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fac_pos&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">fac</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">zero_lt_one</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fac</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">mul_pos</span><span class="w"> </span><span class="n">n.succ_pos</span><span class="w"> </span><span class="o">(</span><span class="n">fac_pos&#39;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span>
</pre></div>
</div>
<p>Notice also the absence of the <code class="docutils literal notranslate"><span class="pre">:=</span></code>, the <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">n</span></code> after the colon, the <code class="docutils literal notranslate"><span class="pre">by</span></code> keyword in each case,
and the inductive appeal to <code class="docutils literal notranslate"><span class="pre">fac_pos'</span> <span class="pre">n</span></code>.
It is as though the theorem is a recursive function of <code class="docutils literal notranslate"><span class="pre">n</span></code> and in the inductive step we make
a recursive call.</p>
<p>This style of definition is remarkably flexible.
Lean&#8217;s designers have built in elaborate means of defining recursive functions, and these
extend to doing proofs by induction.
For example, we can define the Fibonacci function with multiple base cases.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[</span><span class="n">simp</span><span class="kd">]</span><span class="w"> </span><span class="kd">def</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="mi">0</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="mi">1</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">&#64;[simp]</span></code> annotation means that the simplifier will use the defining equations.
You can also apply them by writing <code class="docutils literal notranslate"><span class="pre">rw</span> <span class="pre">[fib]</span></code>.
Below it will be helpful to give a name to the <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">+</span> <span class="pre">2</span></code> case.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fib_add_two</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fib</span><span class="o">]</span>
</pre></div>
</div>
<p>Using Lean&#8217;s notation for recursive functions, you can carry out proofs by induction on the
natural numbers that mirror the recursive definition of <code class="docutils literal notranslate"><span class="pre">fib</span></code>.
The following example provides an explicit formula for the nth Fibonacci number in terms of
the golden mean, <code class="docutils literal notranslate"><span class="pre">&#966;</span></code>, and its conjugate, <code class="docutils literal notranslate"><span class="pre">&#966;'</span></code>.
We have to tell Lean that we don&#8217;t expect our definitions to generate code because the
arithmetic operations on the real numbers are not computable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span>

<span class="kd">def</span><span class="w"> </span><span class="n">phi</span><span class="w">  </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">&#8730;</span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>
<span class="kd">def</span><span class="w"> </span><span class="n">phi&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="bp">&#8730;</span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">phi_sq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">phi</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">phi</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">field_simp</span><span class="w"> </span><span class="o">[</span><span class="n">phi</span><span class="o">,</span><span class="w"> </span><span class="n">add_sq</span><span class="o">]</span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">phi&#39;_sq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">phi&#39;</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">phi&#39;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">field_simp</span><span class="w"> </span><span class="o">[</span><span class="n">phi&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">sub_sq</span><span class="o">]</span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">fib_eq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">phi</span><span class="bp">^</span><span class="n">n</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">phi&#39;</span><span class="bp">^</span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#8730;</span><span class="mi">5</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w">   </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">1</span><span class="w">   </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">field_simp</span><span class="w"> </span><span class="o">[</span><span class="n">phi</span><span class="o">,</span><span class="w"> </span><span class="n">phi&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="bp">+</span><span class="mi">2</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">field_simp</span><span class="w"> </span><span class="o">[</span><span class="n">fib_eq</span><span class="o">,</span><span class="w"> </span><span class="n">pow_add</span><span class="o">,</span><span class="w"> </span><span class="n">phi_sq</span><span class="o">,</span><span class="w"> </span><span class="n">phi&#39;_sq</span><span class="o">]</span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>Induction proofs involving the Fibonacci function do not have to be of that form.
Below we reproduce the <code class="docutils literal notranslate"><span class="pre">Mathlib</span></code> proof that consecutive Fibonacci numbers are coprime.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fib_coprime_fib_succ</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Coprime</span><span class="w"> </span><span class="o">(</span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">fib</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.coprime_add_self_right</span><span class="o">]</span>
<span class="w">    </span><span class="n">exact</span><span class="w"> </span><span class="n">ih.symm</span>
</pre></div>
</div>
<p>Using Lean&#8217;s computational interpretation, we can evaluate the Fibonacci numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#eval</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="mi">6</span>
<span class="k">#eval</span><span class="w"> </span><span class="n">List.range</span><span class="w"> </span><span class="mi">20</span><span class="w"> </span><span class="bp">|&gt;.</span><span class="n">map</span><span class="w"> </span><span class="n">fib</span>
</pre></div>
</div>
<p>The straightforward implementation of <code class="docutils literal notranslate"><span class="pre">fib</span></code> is computationally inefficient. In fact, it runs
in time exponential in its argument. (You should think about why.)
In Lean, we can implement the following tail-recursive version, whose running time is linear
in <code class="docutils literal notranslate"><span class="pre">n</span></code>, and prove that it computes the same function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">fib&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">aux</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="mi">1</span>
<span class="n">where</span><span class="w"> </span><span class="n">aux</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w">   </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">x</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="bp">+</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">aux</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">fib&#39;.aux_eq</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fib&#39;.aux</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">(</span><span class="n">fib</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">))</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">generalizing</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">fib&#39;.aux</span><span class="o">]</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">fib&#39;.aux</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="n">fib_add_two</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">,</span><span class="w"> </span><span class="n">add_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">fib&#39;_eq_fib</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fib&#39;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="n">erw</span><span class="w"> </span><span class="o">[</span><span class="n">fib&#39;</span><span class="o">,</span><span class="w"> </span><span class="n">fib&#39;.aux_eq</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="n">n</span><span class="o">]</span><span class="bp">;</span><span class="w"> </span><span class="n">rfl</span>

<span class="k">#eval</span><span class="w"> </span><span class="n">fib&#39;</span><span class="w"> </span><span class="mi">10000</span>
</pre></div>
</div>
<p>Notice the <code class="docutils literal notranslate"><span class="pre">generalizing</span></code> keyword in the proof of <code class="docutils literal notranslate"><span class="pre">fib'.aux_eq</span></code>.
It serves to insert a <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">m</span></code> in front of the inductive hypothesis, so that in the induction
step, <code class="docutils literal notranslate"><span class="pre">m</span></code> can take a different value.
You can step through the proof and check that in this case, the quantifier needs to be
instantiated to <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">+</span> <span class="pre">1</span></code> in the inductive step.</p>
<p>Notice also the use of <code class="docutils literal notranslate"><span class="pre">erw</span></code> (for &#8220;extended rewrite&#8221;) instead of <code class="docutils literal notranslate"><span class="pre">rw</span></code>.
This is used because to rewrite the goal <code class="docutils literal notranslate"><span class="pre">fib'.aux_eq</span></code>, <code class="docutils literal notranslate"><span class="pre">fib</span> <span class="pre">0</span></code> and <code class="docutils literal notranslate"><span class="pre">fib</span> <span class="pre">1</span></code>
have to be reduced to <code class="docutils literal notranslate"><span class="pre">0</span></code> and <code class="docutils literal notranslate"><span class="pre">1</span></code>, respectively.
The tactic <code class="docutils literal notranslate"><span class="pre">erw</span></code> is more aggressive than <code class="docutils literal notranslate"><span class="pre">rw</span></code> in unfolding definitions to
match parameters.
This isn&#8217;t always a good idea; it can waste a lot of time in some cases, so use <code class="docutils literal notranslate"><span class="pre">erw</span></code>
sparingly.</p>
<p>Here is another example of the <code class="docutils literal notranslate"><span class="pre">generalizing</span></code> keyword in use, in the proof of another
identity that is found in <code class="docutils literal notranslate"><span class="pre">Mathlib</span></code>.
An informal proof of the identity can be found <a class="reference external" href="https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers">here</a>.
We provide two variants of the formal proof.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">fib_add</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">generalizing</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">succ</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">    </span><span class="n">specialize</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_assoc</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="n">n</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">ih</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">fib_add_two</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.succ_eq_add_one</span><span class="o">,</span><span class="w"> </span><span class="n">ih</span><span class="o">]</span>
<span class="w">    </span><span class="n">ring</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">fib_add&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">_</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w">     </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="k">have</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">fib_add&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="n">n</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_assoc</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="n">n</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">fib_add_two</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.succ_eq_add_one</span><span class="o">,</span><span class="w"> </span><span class="n">this</span><span class="o">]</span>
<span class="w">    </span><span class="n">ring</span>
</pre></div>
</div>
<p>As an exercise, use <code class="docutils literal notranslate"><span class="pre">fib_add</span></code> to prove the following.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">):</span><span class="w"> </span><span class="o">(</span><span class="n">fib</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">))</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">fib</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Lean&#8217;s mechanisms for defining recursive functions are flexible enough to allow arbitrary
recursive calls, as long the complexity of the arguments decrease according to some
well-founded measure.
In the next example, we show that every natural number <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&#8800;</span> <span class="pre">1</span></code> has a prime divisor,
using the fact that if <code class="docutils literal notranslate"><span class="pre">n</span></code> is nonzero and not prime, it has a smaller divisor.
(You can check that Mathlib has a theorem of the same name in the <code class="docutils literal notranslate"><span class="pre">Nat</span></code> namespace,
though it has a different proof than the one we give here.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="bp">@</span><span class="n">Nat.not_prime_iff_exists_dvd_lt</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="bp">&#8704;</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">},</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#172;</span><span class="n">Nat.Prime</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="o">))</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">ne_one_iff_exists_prime_dvd</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="o">},</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">p.Prime</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">n</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Exists.intro</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="n">Nat.prime_two</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.not_prime_one</span><span class="o">]</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="k">have</span><span class="w"> </span><span class="n">hn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="bp">+</span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">omega</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">Ne</span><span class="o">,</span><span class="w"> </span><span class="n">not_false_iff</span><span class="o">,</span><span class="w"> </span><span class="n">true_iff</span><span class="o">,</span><span class="w"> </span><span class="n">hn</span><span class="o">]</span>
<span class="w">    </span><span class="n">by_cases</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.Prime</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">n</span><span class="bp">+</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="n">h</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">omega</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Nat.not_prime_iff_exists_dvd_lt</span><span class="w"> </span><span class="n">this</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span>
<span class="w">      </span><span class="n">rcases</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mdvdn</span><span class="o">,</span><span class="w"> </span><span class="n">mge2</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="o">&#10217;</span>
<span class="w">      </span><span class="k">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">omega</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">ne_one_iff_exists_prime_dvd</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">this</span>
<span class="w">      </span><span class="n">rcases</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">primep</span><span class="o">,</span><span class="w"> </span><span class="n">pdvdm</span><span class="o">&#10217;</span>
<span class="w">      </span><span class="n">use</span><span class="w"> </span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">primep</span>
<span class="w">      </span><span class="n">exact</span><span class="w"> </span><span class="n">pdvdm.trans</span><span class="w"> </span><span class="n">mdvdn</span>
</pre></div>
</div>
<p>The line <code class="docutils literal notranslate"><span class="pre">rw</span> <span class="pre">[ne_one_iff_exists_prime_dvd]</span> <span class="pre">at</span> <span class="pre">this</span></code> is like a magic trick: we are using
the very theorem we are proving in its own proof.
What makes it work is that the inductive call is instantiated at <code class="docutils literal notranslate"><span class="pre">m</span></code>,
the current case is <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">+</span> <span class="pre">2</span></code>, and the context has <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&lt;</span> <span class="pre">n</span> <span class="pre">+</span> <span class="pre">2</span></code>.
Lean can find the hypothesis and use it to show that the induction is well-founded.
Lean is pretty good at figuring out what is decreasing; in this case, the choice of
<code class="docutils literal notranslate"><span class="pre">n</span></code> in the statement of the theorem and the less-than relation is obvious.
In more complicated cases, Lean provides mechanisms to provide this information
explicitly. See the section on <a class="reference external" href="https://lean-lang.org/doc/reference/latest//Definitions/Recursive-Definitions/#well-founded-recursion">well-founded recursion</a> in the Lean Reference Manual.</p>
<p>Sometimes, in a proof, you need to split on cases depending on whether a natural number <code class="docutils literal notranslate"><span class="pre">n</span></code>
is zero or a successor, without requiring an inductive hypothesis in the successor case.
For that, you can use the <code class="docutils literal notranslate"><span class="pre">cases</span></code> and <code class="docutils literal notranslate"><span class="pre">rcases</span></code> tactics.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">zero_lt_of_mul_eq_one</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">cases</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">cases</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="bp">*</span><span class="n">m</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">(</span><span class="n">_</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="bp">;</span><span class="w"> </span><span class="n">simp</span>
<span class="w">  </span><span class="n">rcases</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">(</span><span class="n">_</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>This is a useful trick.
Often you have a theorem about a natural number <code class="docutils literal notranslate"><span class="pre">n</span></code> for which the zero case is easy.
If you case on <code class="docutils literal notranslate"><span class="pre">n</span></code> and take care of the zero case quickly, you are left with the original
goal with <code class="docutils literal notranslate"><span class="pre">n</span></code> replaced by <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">+</span> <span class="pre">1</span></code>.</p>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C04_Sets_and_Functions.html" class="btn btn-neutral float-left" title="4. Sets and Functions" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C06_Discrete_Mathematics.html" class="btn btn-neutral float-right" title="6. Discrete Mathematics" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>